\documentclass[10pt]{beamer}

\input{packages}
\input{lpar2008.def}

 
\mode<presentation>
{
  \usetheme{Berlin}  %% \usetheme{default} 
  \setbeamercovered{transparent}
  \usecolortheme{seahorse}
  \usecolortheme{rose} %% \usecolortheme{crane} % (oranje)
  \setbeamertemplate{navigation symbols}{}
\setbeamertemplate{itemize items}[triangle]
\setbeamertemplate{sections/subsections in toc}[sections numbered]
%\setbeamercolor{math text}{fg=black}
}

%------------------------------------------------------------------------


%%\usepackage[german]{babel}
% oder was auch immer

\usepackage[latin1]{inputenc}
% oder was auch immer

\usepackage{times}
\usepackage[T1]{fontenc}
% Oder was auch immer. Zu beachten ist, das Font und Encoding passen
% m�ssen. Falls T1 nicht funktioniert, kann man versuchen, die Zeile
% mit fontenc zu l�schen.


\title{Data-Oblivious Stream Productivity}

%\title[Watching Streams Grow]{\scalebox{0.99}%
%         {\hspace*{-1.5pt}Watching \hspace*{-1.5pt}Streams \hspace*{-1.5pt}Grow: 
%          \hspace*{-1.5pt}The \hspace*{-1.5pt}Pebbleflow \hspace*{-1.5pt}Method}}

\author[Endrullis, Grabmayer, Hendriks]{
  J\"{o}rg Endrullis         %\inst{1}
  \and {Clemens Grabmayer}   %\inst{2}
  \and Dimitri Hendriks      \\%\inst{1}
}

%% \institute{
%%   Universiteit Utrecht, 
%%   Vrije Universiteit
%%                               \\[2ex]
%% {\chocolate{\large NWO-Bricks Project Infinity}}  %{{ $\boldsymbol{\infty}$}}
%%           }
  
%% \institute{
%%   Department of Philosophy, \emph{Universiteit Utrecht}\\[0.5ex]
%%   Department of Computer Science, \emph{Vrije Universiteit}\\[0.5ex]
%%   Department of Computer Science, \emph{Radboud Universiteit}   
%%            }

\institute[LPAR 2008]{%
  Vrije Universiteit Amsterdam~--~Universiteit Utrecht%
  ~--~Vrije Universiteit Amsterdam\\[1ex]
  The Netherlands}

\date{
  {\forestgreen{LPAR 2008}, \emph{Doha, Qatar}\\[1ex] 
      23--27 Nov, 2008}
      }


\subject{Informatik}
% Dies wird lediglich in den PDF Informationskatalog einf�gt. Kann gut
% weggelassen werden.


% Falls eine Logodatei namens "university-logo-filename.xxx" vorhanden
% ist, wobei xxx ein von latex bzw. pdflatex lesbares Graphikformat
% ist, so kann man wie folgt ein Logo einf�gen:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}


%% % Folgendes sollte gel�scht werden, wenn man nicht am Anfang jedes
%% % Unterabschnitts die Gliederung nochmal sehen m�chte.
%   \AtBeginSection[]
%   {
%   \begin{frame}<beamer>
%     \frametitle{Overview}
%     \tableofcontents[currentsection] %[...,currentsubsection]
%   \end{frame}
%    }


% Falls Aufz�hlungen immer schrittweise gezeigt werden sollen, kann
% folgendes Kommando benutzt werden:

%\beamerdefaultoverlayspecification{<+->}



%----------------------------------------------------------------

\begin{document}

%\renewcommand{\pause}{}



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\titlepage

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\setcounter{tocdepth}{1}

%------------------------------------------------------------------------
%------------------------------------------------------------------------
\section{Productivity}
%------------------------------------------------------------------------
%------------------------------------------------------------------------

%------------------------------------------------------------------------
%\subsection{Productivity. Previous Approaches.}
%------------------------------------------------------------------------



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Specifying Streams}


\begin{itemize}\setlength{\itemsep}{3mm plus1mm minus1mm}
  %
  %\item $\str{A} \defdby \{ \astr \where \astr \funin {\nat\to A} \}$ the set of streams over $A$.
    %
  \item A \emph{stream} over $A$ is an infinite sequence of elements from $A$.
    %
  \item Using the \emph{stream constructor symbol {\tt "}$\sstrcns${\tt "}},
    we write streams as:\vspace*{-0.5ex}% infinite terms:\vspace*{-0.5ex}
    \[\emph{\strcns{\datsymb{a_0}}{\strcns{\datsymb{a_1}}{\strcns{\datsymb{a_2}}{\ldots}}}} .\]
   %% where `$\sstrcns$' is the stream constructor symbol.
   %
\end{itemize}
%
  %\item %Example of a specification of the \emph{Thue--Morse stream}:
    %
%\vspace*{-0.0ex}
%
\begin{example}[Thue--Morse stream]
  %
  \vspace*{-0.75ex}
  %
\begin{center}
\scalebox{1}{
\renewcommand{\arraystretch}{1.3}
\begin{tabular}{r@{\hspace*{1.5ex}}cr}
  \hline
  &
  $\morse \red \strcns{\datsymb{0}}{\strcns{\datsymb{1}}{\strfff{f}{\strtl{\morse}}}}$
  & {\it stream constant}\\[0.5ex]
  &
  $\strfff{f}{\strcns{x}{\astr}} 
     \red
   \strcns{x}{\strcns{\funap{\datf{i}}{x}}{\strfff{f}{\astr}}}
  $ 
 & \quad  
  \multirow{2}{*}{{\it stream functions}}
  \\[-0.0ex]
  &
  $\strtl{\strcns{x}{\astr}} \red \astr$
  \\[-0.0ex]
  \hline
  &
  $\funap{\datsymb{i}}{\datsymb{0}} \red \datsymb{1} \quad\quad \funap{\datsymb{i}}{\datsymb{1}} \red \datsymb{0}$
  & {\it data functions} \\
  \hline
\end{tabular}
               }
\end{center}
%
%% \begin{center}
%% \scalebox{1}{
%% \renewcommand{\arraystretch}{1.3}
%% \begin{tabular}{r@{\hspace*{1.5ex}}cr}
%%   \hline
%%   &
%%   $\morse \red \strcns{\datsymb{0}}{\strcns{\datsymb{1}}{\strzip{\strtl{\morse}}{\strinv{\strtl{\morse}}}}}$ 
%%   & {\it stream constant}\\[0.5ex]
%%   &
%%   $\strtl{\strcns{x}{\astr}} \red \astr$ & \\[-0.0ex]
%%   &
%%   $\strzip{\strcns{x}{\astr}}{\bstr} \red \strcns{x}{\strzip{\bstr}{\astr}}$%%  
%%   & {\it stream functions} \\[-0.0ex]
%%   &
%%   $\strinv{\strcns{x}{\astr}} \red \strcns{\funap{\datsymb{i}}{x}}{\strinv{\astr}}$ & \\
%%   \hline
%%   &
%%   $\funap{\datsymb{i}}{\datsymb{0}} \red \datsymb{1} \quad\quad \funap{\datsymb{i}}{\datsymb{1}} \red \datsymb{0}$
%%   & {\it data functions} \\
%%   \hline
%% \end{tabular}
%%                }
%% \end{center}
 
\vspace*{0.5ex} 
%
{It holds:  }
  \scalebox{1}{
  $
  \morse \infred \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{1}}\strcns{\datf{0}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{0}}\strcns{\datf{1}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{0}}\strcns{\datf{1}}{
                 \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{1}}\strcns{\datf{0}}{
                   \ldots}}}}}}}}}}}}
  $
  }
 %
\end{example}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Productivity}

\hspace*{-5ex}
\begin{itemize}
    %
  \item 
    captures: \emph{unlimited production of well-defined values}\\
    %when programming with 
    for infinite data types;
    %of `working' programs, producing defined values indefinitely; 
    %
    \vspace*{1ex}
    %
  \item corresponds to:
    \emph{termination in a well-defined result}\\
    %when programming with
    for finite data types;
    %
    \vspace*{1ex}
    %
  \item a stream specification  
    %% \[
    %%   \astrcon = \ldots\, {\astrcon} \,\ldots
    %% \]
    is \magenta{productive}
    if lazy/fair evaluation of its root
    $\rootsc$ results in an infinite \emph{constructor normal form}:
    \[
      \rootsc
      \infred
      \strcns{\datsymb{a_0}}{\strcns{\datsymb{a_1}}{\strcns{\datsymb{a_2}}{\ldots}}}
    \; .
    \]
  %
  \item  highly \emph{undecidable}
    (basic version \emph{$\Pi^0_2$-complete}, others \emph{worse}). 
    %
    \vspace*{1ex}
    %
  \item but for \forestgreen{restricted formats} 
    \emph{computable sufficient conditions}
    or \emph{decidability} can be obtained.
  %%   %
  %%   \vspace*{1ex}
  %%   %
  %% \item in principle 
  %%   \emph{reducible to a termination-and-well-definedness problem},
  %%   but direct methods of proving productivity are desirable.
    %
\end{itemize}
              
\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification}

\begin{example}
  %
  \vspace*{0.5ex}
  %
\begin{center}
\scalebox{1}{ 
\renewcommand{\arraystretch}{1.3}
\begin{tabular}{r@{\hspace*{1.5ex}}cr}
  \hline
  &
  $\morse \red 
   \strcns{\datf{0}}{\strcns{\datf{1}}{\strfff{f}{\strtl{\morse}}}}$ 
  \\[-0.0ex]
  &
  $\strfff{f}{\strcns{\datf{0}}{\astr}} 
     \red
   \strcns{\datf{0}}{\strcns{\datf{1}}{\strfff{f}{\astr}}}
  $  
  & {\it stream layer}
  \\[-0.0ex]
  &
  $\strfff{f}{\strcns{\datf{1}}{\astr}} 
     \red
   \strcns{\datf{1}}{\strcns{\datf{0}}{\strfff{f}{\astr}}}
  $
  \\[-0.0ex]
  &
  $\strtl{\strcns{x}{\astr}} \red \astr$
  \\[-0.0ex]
  \hline
  & & {\it data layer}
  \\
  \hline
\end{tabular}
               }
\end{center}
  %
  \mbox{}\\[-0.5ex]
  %
\end{example}
 
\vspace*{-1.5ex}
%
\begin{flushleft}
  \scalebox{1}{is a \emph{productive} stream definition
               of the \emph{Thue--Morse stream}:}\\[1.5ex]
  \hspace*{\fill}
  \scalebox{1}{
  $
  \morse \infred \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{1}}\strcns{\datf{0}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{0}}\strcns{\datf{1}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{0}}\strcns{\datf{1}}{
                 \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{1}}\strcns{\datf{0}}{
                   \ldots}}}}}}}}}}}}
  $
                  }\hspace*{\fill}
\end{flushleft}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification}

\begin{example}%[not productive Stream Spec]
  %
  \vspace*{-0.75ex}
  %
\begin{center}
\scalebox{1}{
\renewcommand{\arraystretch}{1.25}
\begin{tabular}{r@{\hspace{1.5ex}}cr}
  \hline
  &
  $\joerg 
      = \strcns{\datsymb{0}}{\strcns{\datsymb{1}}{\strev{\joerg}}}$
  \\
  &
  $\strev{\strcns{x}{\astr}} \red \strcns{x}{\strod{\astr}}$ & {\it stream layer} \\[-0.0ex]
  &
  $\strod{\strcns{x}{\astr}} \red \strev{\astr} $ 
  \\[-0.0ex]
  \hline
  &
  \phantom{
    $\funap{\datsymb{i}}{\datsymb{0}} \red \datsymb{1}\quad\quad \funap{\datsymb{i}}{\datsymb{1}} \red \datsymb{0}$
          }
  & {\it data layer}\\
  \hline
\end{tabular}
               }
\end{center}
\end{example}
%
\begin{flushleft}
  \scalebox{1}{is \emph{not productive}:}\\[1.5ex]
  \hspace*{\fill}
  \scalebox{1}{
  $
  \joerg \infred \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{0}}\strcns{\datf{0}}{
  \strev{\strev{\ldots}}
                                % {{{{     \sstrev^{\omega}}}}}
         }}}
  $
                  }\hspace*{\fill}
\end{flushleft}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification}

\begin{example}
  %
  \vspace*{0.5ex}
  %
\begin{center}
\scalebox{1}{ 
  \renewcommand{\arraystretch}{1.3}
  \begin{tabular}{r@{\hspace{0ex}}r@{\extracolsep{.5ex}}c@{\extracolsep{.5ex}}lr}
    \hline
    \multicolumn{4}{c}{
    $\strcf{P} \red \strcns{\numzer}{\strcns{\numsuc{\numzer}}{\funap{\strff{g}}{\strcf{P}}}}$} 
    \\
    &$\funap{\strff{g}}{\strcns{\numsuc{x}}{\strcns{y}{\astr}}}$ 
    &$\red$& $\strcns{\numadd{\numsuc{x}}{y}}{\funap{\strff{g}}{\strcns{y}{\astr}}}$%  & \text{\textit{stream layer}}
    & {\it stream layer} \\
    &$\funap{\strff{g}}{\strcns{\numzer}{\astr}}$ 
    &$\red$& $\strcns{\numzer}{\strcns{\numsuc{\numzer}}{\funap{\strff{g}}{\astr}}}$
    \\
    \hline
    &$\numadd{x}{\numsuc{y}}$ 
    &$\red$& $\numsuc{\numadd{x}{y}}$ 
    & \multirow{2}{*}{\text{\textit{data layer}}}
    \\[-0.5ex]
    &$\numadd{x}{\numzer}$ 
    &$\red$& $x$
    \\
    \hline
  \end{tabular}
}
\end{center}
  %
  \mbox{}\\[-0.5ex]
  %
\end{example}
 
\vspace*{-1.5ex}
%
\begin{flushleft}
  \scalebox{1}{is a \emph{productive} stream definition
               of the \emph{Pascal's triangle}:}\\[1.5ex]
  \hspace*{\fill}
  \scalebox{1}{
  $
  \strcf{P} \infred \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{0}}\strcns{\datf{1}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{1}}\strcns{\datf{2}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{1}}\strcns{\datf{3}}{
                 \strcns{\datf{3}}{\strcns{\datf{1}}{\strcns{\datf{0}}{
                   \ldots}}}}}}}}}}}}
  $
                  }\hspace*{\fill}
\end{flushleft}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%------------------------------------------------------------------------
%------------------------------------------------------------------------
\section{Stream Specifications}
%------------------------------------------------------------------------
%------------------------------------------------------------------------



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{}%{Stream Specifications}

We formalize stream specifications as:
\begin{itemize}
 \item $\{\sortS,\sortD\}$-sorted, orthogonal, constructor TRSs $\atrs = \pair{\asig}{R}$
 \item $\Ss$ \emph{stream symbols} and $\Sd$ \emph{data symbols}
 %\item $\text{`$\sstrcns$'} \in \Ss$, the \emph{stream constructor symbol}, with arity $\sortD\times\sortS \to \sortS$
\end{itemize}

\begin{definition}[Stream Specification]
  %
  \begin{center}
  \renewcommand{\arraystretch}{1.3}
  \begin{tabular}{crc}
    \cline{1-2}
    $\Rs$ & {\em stream layer}\\
      \cline{1-2}
    $\Rd$ & {\em data layer}\\
    \cline{1-2}
  \end{tabular}
  \end{center}
  %
  \begin{enumerate}
    \item $\rootsc \in \Ss$ with arity 0, the \emph{root of\/ $\atrs$}.
    \item\label{def:scs:data}
       $\pair{\Sd}{\Rd}$ is a terminating, $\sortD$-sorted TRS, the \emph{data layer} of\/ $\atrs$.
    \item\label{def:scs:exhaustive}
      $\atrs$ is exhaustive% (for all defined symbols in $\asig = \Ss \uplus \Sd$).
  \end{enumerate}
\end{definition}

%\pause

% Excludes: $\strhd{\strcns{x}{\astr}} \to x$.
% %
% But e.g.\ a function like:
% \vspace{-.5ex}
% \[\bfunap{\astrfun}{\astr}{\bstr} \red \strcns{(\strhd{\astr} + \strhd{\bstr})}{\bfunap{\astrfun}{\strtl{\astr}}{\strtl{\bstr}}}\]
% %
% %\vspace{-3ex}
% can be replaced by:
% \vspace{-1ex}
% \[ \qquad
%    \bfunap{\astrfun}{\strcns{x}{\astr}}{\strcns{y}{\bstr}} \red \strcns{(x + y)}{\bfunap{\astrfun}{\astr}{\bstr}} \;.\]
 
\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Productivity Recognition: Previous Approaches}

\begin{itemize}
%   %
%   \item concept/name introduced by \emph{Dijkstra (1980)};
%     %
%     \vspace*{0.75ex}
%     %
  \item \emph{Wadge (1981)}: `cyclic sum test'
    %(\forestgreen{limited, computable criterion}).
    %
    \vspace*{0.75ex}
    %
  \item \emph{Sijtsma (1989)}: mathematical theory % of productivity
    with `production moduli' 
    %(\forestgreen{mathem., not directly computable criteria}).\pause{}
    %
    \vspace*{0.75ex}
    %
  \item \emph{Coquand (1994)}: `guardedness' as a syntactic criterion
    %for productivity 
    %(\forestgreen{automatable}, but \forestgreen{restrictive criterion}).
    %
    \vspace*{0.75ex}
    %
  \item \emph{Telford and Turner (1997)}: method in the flavour of Wadge %: extend the notion of
    %guardedness by a method in the flavour of Wadge.
    %
    \vspace*{0.75ex}
    %
  \item \emph{Hughes, Pareto, and Sabry (1996)}: type system
    %for proving productivity (\forestgreen{automatable criterion}).\pause{}
    %
    \vspace*{0.75ex}
    %
  \item \emph{Buchholz (2004)}: two type systems % for proving productivity,
    %% two forms:
    %%%
   %% \vspace*{-1.5ex}
    %
    %%\begin{itemize}
    %%  %
    %%  \item using unrestricted production moduli 
    %%    (\forestgreen{general, not automatable});
    %%    %
    %%  \item a decidable subsystem with limited moduli
    %%    (\forestgreen{automable criterion}, 
    %%     handles all examples of Telford \&Turner).\pause{}
    %%    %
    %%\end{itemize}
    %
\end{itemize}

\alert{Common essence} of all previous approaches: \alert{data-oblivious analysis}

\hfill{\ldots more on the next slide}
\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Data-Oblivious Analysis}

Data-oblivious analysis is a \emph{data blind judgement about productivity}:
\begin{itemize}
 \item quantitative analysis that 
 \item abstraction from concrete data values
\end{itemize}\ \\[1ex]

Why did all previous approaches choose a data-oblivious analysis?
\begin{itemize}
 \item data-aware productivity is highly undecidable
 \item for example for a specification of a bit stream $\strcf{T}$\\
       it is not decidable whether the stream $\strcf{T}$ contains a $\datf{1}$.
\end{itemize}\ \\[1ex]

What we do:
\begin{itemize}
 \item we \emph{formalize the concept of data-oblivious rewritig},
 \item thereby \emph{showing the theoretical limitations}, and
 \item we devise a \emph{data-oblivious optimal analysis}.
\end{itemize}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%------------------------------------------------------------------------
%\subsection{First Paper. New Results.}
%------------------------------------------------------------------------



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{New Concepts/Definitions}


\begin{itemize}
  %
  \item \emph{data-oblivious rewriting};
    %
    \vspace*{0.15ex}
    %
  \item \emph{data-oblivious productivity};
    %
    \vspace*{0.15ex}
    %
  \item stream specification formats: 
    $ \text{\emph{pure}}
        \subsetneq
      \text{\emph{flat}}
        \subsetneq 
      \text{\emph{friendly nesting}} $.
    %
\end{itemize}


\begin{center}
  %
  \scalebox{0.8}{ 
    \includegraphics{figs/pstricks/pnp}
              }
  %
\end{center}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Results}

\begin{enumerate}
  %
  \item \label{item:flat}
    for \emph{flat} stream spec's:\\ a 
    \emph{decision method for data-oblivious productivity},
    yielding a
    \chocolate{computable, data-obliviously optimal criterion
    for productivity};
    %
    \vspace*{0.15ex}
    %
  \item \label{item:pure}
    for \emph{pure} stream spec's: 
    a \chocolate{decision method for productivity}; 
    %
    \vspace*{0.15ex}
    %
  \item \label{item:fn}
    for \emph{friendly nesting} stream spec's: 
    a \chocolate{computable criterion for productivity}; 
    %
    \vspace*{0.15ex}
    %
  \item an \chocolate{online-tool} automating (\ref{item:flat}),
    (\ref{item:pure}), and (\ref{item:fn}). 
    %
\end{enumerate}

\vspace*{-0.75ex}
%
\begin{center}
  %
  \scalebox{0.7}{ 
    \includegraphics{figs/pstricks/pnp}
              }
  %
\end{center}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%------------------------------------------------------------------------
%------------------------------------------------------------------------
\section[D-O Analysis]{Data-Oblivious Analysis}
%------------------------------------------------------------------------
%------------------------------------------------------------------------
%------------------------------------------------------------------------
%\subsection{}
%------------------------------------------------------------------------


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Data-Oblivious Rewriting}

We formalize data-oblivious rewriting as a \emph{two-player game}:
%
\begin{itemize}
  %
  \item \emph{rewrite player} $\mathcal{R}$ 
    can perform usual term rewriting steps
    %
  \item \emph{data-exchange player} $\sdg$ can exchange 
        data elements arbitrarily
        %
\end{itemize}\ \\[1ex]

Data-exchange player $\sdg$ can \emph{help or handicap} the rewrite player.\\[1ex]

The strategy of $\sdg$ is not known.
\begin{itemize}
 \item [$\Rightarrow$] We have no knowledge about the data elements during rewriting.
\end{itemize}\ \\[1ex]

Hence the \emph{judgement about productivity in such a game is data-blind}.

\begin{definition}[\emph{Data-oblivious lower bound} on the production of a term $s$]
  \vspace{-2.5ex}
  %
  \begin{align*}
    %
    \doLow{\atrs}{\astrtrm} \;\defdby\;\ &\text{worst case production of $s$ (number of elements)}\\
                                         &\text{with respect to all strategies for $\sdg$}
    %
  \end{align*}
  %
  A stream spec~$\atrs$ is \emph{data-obliviously productive} if $\doLow{\atrs}{\rootsc} = \infty$.
\end{definition}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Data-oblivious productivity implies productivity}

\begin{proposition}
  The data oblivious production is always $\le$ the data aware production:
  \begin{equation*}
    %
    \doLow{\atrs}{s} \le \terprd{\atrs}{s} \; .
    %
  \end{equation*}
  %
  Hence, data-oblivious productivity implies productivity.
\end{proposition}

\begin{proof}
  A possible strategy for the exchange player $\sdg$ is `do nothing'.
\end{proof}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Example, Limits of Data-Oblivious Analysis}

\begin{example}
\begin{align*}
  \strcf{T} &\red \funap{\strff{f}}{\strcns{\datf{1}}{\strcf{T}}} &
  \strfunap{f}{ \strcns{\datf{0}}{\astr} } &\red \strfunap{f}{\astr} &
  \strfunap{f}{\strcns{\datf{1}}{\astr}} &\red \strcns{1}{\strfunap{f}{\astr}}
\end{align*}
\end{example}

% \begin{center}
%   %
% \scalebox{1}{
% \renewcommand{\arraystretch}{1.25}
% \begin{tabular}{r@{\hspace{1.5ex}}cr}
%   \hline
%   &
%   $\strcf{T} \red \funap{\strff{f}}{\strcns{\datf{1}}{\strcf{T}}}$
%   & \multirow{3}{*}{\it stream layer}
%   \\
%   $(\rho_{\astrfunsub\datf{0}}):$\hspace*{2ex}
%   &
%   $\strfunap{f}{ \strcns{\datf{0}}{\astr} } \red \strfunap{f}{\astr}$
%   \\
%   $(\rho_{\astrfunsub\datf{1}}):$\hspace*{2ex} 
%   &
%   $\strfunap{f}{\strcns{\datf{1}}{\astr}} \red \strcns{1}{\strfunap{f}{\astr}}$
%   &
%   \\
%   \hline
%   & & {\it data layer}\\
%   \hline
% \end{tabular}
%   %
%   }
%   %
% \end{center}


This specification is \emph{productive}:
%
\begin{equation*}
  %
  \strcf{T} 
    \mred \strcns{\datf{1}}{\funap{\strff{f}}{\strcf{T}}}
    \mred \strcns{\datf{1}}{\strcns{\datf{1}}{\funap{\strff{f}}{\funap{\strff{f}}{\strcf{T}}}}}
    \mred \ldots 
    \infred \strcns{\datf{1}}{\strcns{\datf{1}}{\strcns{\datf{1}}{\strcns{\datf{1}}{\ldots}}}} \; ,
    %
\end{equation*}
%
but, \emph{disregarding the identity of data}, the rewrite sequence:
%
\begin{equation*}
  %
  \strcf{T}
    \red \funap{\strff{f}}{\strcns{\trspeb}{\strcf{T}}}
    \red^{\rho_{\astrfunsub\datf{1}}}
    \funap{\strff{f}}{\strcf{T}}
    \mred 
    \ldots
    \infred 
    \funap{\strff{f}}{\funap{\strff{f}}{\funap{\strff{f}}{\ldots}}} \; .
    %
\end{equation*}
%
is possible.
%
Hence the specification is 
\alert{not data-obliviously productive}.
(that is, productivity of this specification cannot be proven data blindly)


\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%





\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{D-O Lower Bounds of Stream Functions}

Complex data-oblivious behaviour of a simple stream function spec:
%
\vspace{-1.0ex}
\begin{align*}
% f(s) = g(s,s)
\funap{\strff{f}}{\astr}
&\red \bfunap{\strff{g}}{\astr}{\astr}
\\
% g(0:y:t, x:s) = 0:0:g(s,t)
\bfunap{\strff{g}}{\strcns{\datf{0}}{\strcns{y}{\astr}}}{\strcns{x}{\bstr}}
&\red \strcns{\datf{0}}{\strcns{\datf{0}}{\bfunap{\strff{g}}{\astr}{\bstr}}}
\\
% g(1:t, x1:x2:x3:x4:s) = 1:1:1:1:1:g(s,t)
\bfunap{\strff{g}}{\strcns{\datf{1}}{\astr}}{\strcns{x_1}{\strcns{x_2}{\strcns{x_3}{\strcns{x_4}{\bstr}}}}}
&\red \strcns{\datf{0}}{\strcns{\datf{0}}{\strcns{\datf{0}}{\strcns{\datf{0}}{\strcns{\datf{0}}{\bfunap{\strff{g}}{\astr}{\bstr}}}}}}
\end{align*}
\vspace{-2ex}
%
\begin{center} 
\scalebox{.82}{\includegraphics{figs/pstricks/dobounds}}
\hspace{4ex}
\scalebox{.82}{\includegraphics{figs/pstricks/doboundscmp}}
\end{center}
\vspace{-1ex}
%
\begin{flushleft}
  %
  \hspace*{1.5ex}
  \parbox{150pt}{%
    (small) selection of the\\ possible function-call traces for $\strff{f}$.
                 }
  \hspace*{3.5ex}
  \parbox{90pt}{%
     the data-oblivious\\ lower bound $\doLow{\atrs}{\strff{f}}$.
                 }
  %
\end{flushleft}

% {\it Left:\/} (small) selection of the possible function-call traces for $\strff{f}$.\\
% {\it Right:\/} the data-oblivious lower bound $\doLow{\atrs}{\strff{f}}$.

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%------------------------------------------------------------------------
%------------------------------------------------------------------------
\section{Classes}
%------------------------------------------------------------------------
%------------------------------------------------------------------------

\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Flat Stream Spec's}

$\atrs$ is called \magenta{flat}:
in rules for stream functions,
no nested occurrences\\\hspace*{\fill}
of stream function rules on their right hand sides.

\begin{example}[Ternary Thue-Morse stream]
  % "a" -> "abc", "b" -> "ac", "c" -> "b"
%
\vspace*{-1.25ex}
%
\begin{center}
  \renewcommand{\arraystretch}{1.3}
  %
  \scalebox{0.975}{
  %
  \begin{tabular}{r@{\hspace{1.5ex}}r@{\extracolsep{1ex}}c@{\extracolsep{1ex}}lr}
    \hline
    \multicolumn{4}{c}{
    $\strcf{Q} \red \strcns{\datf{a}}{\strcf{R}}$} & \multirow{5}{*}{\it{stream layer}}\\%[0.5ex]
    \multicolumn{4}{c}{
    $\strcf{R} \red \strcns{\datf{b}}{\strcns{\datf{c}}{\funap{\strff{f}}{\strcf{R}}}}$}
    \\
    &$\funap{\strff{f}}{\strcns{\datf{a}}{\astr}}$ 
    &$\red$& $\strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{\funap{\strff{f}}{\astr}}}}$
    \\%[0.5ex]
    &$\funap{\strff{f}}{\strcns{\datf{b}}{\astr}}$ 
    &$\red$& $\strcns{\datf{a}}{\strcns{\datf{c}}{\funap{\strff{f}}{\astr}}}$ & \\%[0.5ex]
    &$\funap{\strff{f}}{\strcns{\datf{c}}{\astr}}$ 
    &$\red$& $\strcns{\datf{b}}{\funap{\strff{f}}{\astr}}$\\
    \hline
    & & & 
    & \it{data layer} \\
    \hline
  \end{tabular}
  %
  }
  %
\end{center}
%
\vspace*{-1ex}
  %
  $
  \strcf{Q}
  \infred
  \strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{
  \strcns{\datf{a}}{\strcns{\datf{c}}{\strcns{\datf{b}}{
  \strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{
  \strcns{\datf{b}}{\strcns{\datf{a}}{\strcns{\datf{c}}{
  \ldots}}}}}}}}}}}}
  $%
  \hspace*{\fill}\mbox{}
  %
\end{example}

%% \begin{align*}
%%   \strcf{Q} &\red \strcns{\datf{a}}{\strcf{R}} \\
%%   \strcf{R} &\red \strcns{\datf{b}}{\strcns{\datf{c}}{\funap{\strff{f}}{\strcf{R}}}} \\
%%   \funap{\strff{f}}{\strcns{\datf{a}}{\astr}}
%%   &\red \strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{\funap{\strff{f}}{\astr}}}} \\
%%   \funap{\strff{f}}{\strcns{\datf{b}}{\astr}}
%%   &\red \strcns{\datf{a}}{\strcns{\datf{c}}{\funap{\strff{f}}{\astr}}} \\
%%   \funap{\strff{f}}{\strcns{\datf{c}}{\astr}}
%%   &\red \strcns{\datf{b}}{\funap{\strff{f}}{\astr}}
%% \end{align*}
%% \vspace{-2.5ex}

%% \ldots a \emph{productive} specification of the \emph{Ternary Thue-Morse stream}:\\[0.5ex]
%% {\centering
%%   $\strcf{Q} \infred
%%   \strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{
%%   \strcns{\datf{a}}{\strcns{\datf{c}}{\strcns{\datf{b}}{
%%   \strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{
%%   \strcns{\datf{b}}{\strcns{\datf{a}}{\strcns{\datf{c}}{
%%   \ldots}}}}}}}}}}}}$\\[1.0ex]}

% \begin{itemize}
%  \item All defining rules of `$\strff{f}$' are flat, therefore `$\strff{f}$' is flat.
%  \item $\strcf{Q}$ and $\strcf{R}$ are not flat, but stream constant symbols.
%  \item Hence the stream specification is flat.
% \end{itemize}


\begin{theorem}
  For flat stream spec's we can \emph{decide data-oblivious productivity}.
\end{theorem}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Pure Stream Spec's}

$\atrs$ is called \magenta{pure}:
  the defining rules for a stream function $\astrfun$
  all have the same consumption/production behaviour. 

\begin{example}
  %
  \hspace*{1ex}
\parbox[t]{90pt}{
 $\strinv{\strcns{\datf{0}}{\astr}} \red \strcns{\datf{1}}{\strinv{\astr}} \\
  \strinv{\strcns{\datf{1}}{\astr}} \red \strcns{\datf{0}}{\strinv{\astr}}$}
%
\hspace*{15pt}
Non-example: 
\parbox[t]{110pt}{
$\strfunap{f}{ \strcns{\datf{0}}{\strcns{x}{\astr}} } 
 \red \strcns{x}{\strcns{x}{\strfunap{f}{\strcns{\datf{0}}{\astr}}}}$\\
$\strfunap{f}{\strcns{\datf{1}}{\strcns{x}{\astr}}}
 \red \strcns{x}{\strfunap{f}{\strcns{\datf{0}}{\astr}}} \; . $
}
\end{example}

\begin{proposition}[For pure stream specifications \ldots]
  \ldots productivity coincides with data-oblivious productivity.
\end{proposition}

\begin{theorem}
  We can \emph{decide productivity} of pure stream specifications.
\end{theorem}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Friendly Nesting Stream Spec's}

\magenta{Friendly nesting} stream specifications are extensions
of flat ones with \emph{friendly (nesting) rules $\gamma$}:
%
\begin{itemize}
  %
  \item $\gamma$ consumes in each argument at most one stream element,
    %
  \item it produces at least one stream element, and
    %
  \item the defining rules of stream function symbols on the right hand side are friendly again.
  %
\end{itemize}

\begin{example}
\vspace{-1ex}
\begin{center}
  $\bfunap{\strff{f}}{\strcns{x}{\astr}}{\bstr} \red 
   \strcns{x}{\strcns{x}{\funap{\strff{g}}{\bfunap{\strff{f}}{\astr}{\strcns{x}{\bstr}}}}}$ \\[0.5ex]
  $\funap{\strff{g}}{\strcns{x}{\astr}} \red
   \strcns{x}{\funap{\strff{g}}{\strcns{x}{\bfunap{\strff{f}}{\astr}{\astr}}}}$
\end{center}
\vspace{-1ex}
\end{example}

\begin{theorem}[For friendly nesting stream specifications \ldots]
  \ldots we have a sufficient condition for (data-oblivious) productivity.
\end{theorem}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%------------------------------------------------------------------------
%------------------------------------------------------------------------
\section{Examples}
%------------------------------------------------------------------------
%------------------------------------------------------------------------

\begin{comment}
\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification (flat, non-pure)}  


\begin{example}[Ternary Thue--Morse Stream]
  %
  % "a" -> "abc", "b" -> "ac", "c" -> "b"
  %
\begin{center}
  \renewcommand{\arraystretch}{1.3}
  %
  \scalebox{1}{
  %
  \begin{tabular}{r@{\hspace{1.5ex}}r@{\extracolsep{1ex}}c@{\extracolsep{1ex}}lr}
    \hline
    \multicolumn{4}{c}{
    $\strcf{Q} \red \strcns{\datf{a}}{\strcf{R}}$} & \multirow{5}{*}{\it{stream layer}}\\%[0.5ex]
    \multicolumn{4}{c}{
    $\strcf{R} \red \strcns{\datf{b}}{\strcns{\datf{c}}{\funap{\strff{f}}{\strcf{R}}}}$}
    \\
    &$\funap{\strff{f}}{\strcns{\datf{a}}{\astr}}$ 
    &$\red$& $\strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{\funap{\strff{f}}{\astr}}}}$
    \\%[0.5ex]
    &$\funap{\strff{f}}{\strcns{\datf{b}}{\astr}}$ 
    &$\red$& $\strcns{\datf{a}}{\strcns{\datf{c}}{\funap{\strff{f}}{\astr}}}$ & \\%[0.5ex]
    &$\funap{\strff{f}}{\strcns{\datf{c}}{\astr}}$ 
    &$\red$& $\strcns{\datf{b}}{\funap{\strff{f}}{\astr}}$\\
    \hline
    & & & 
    & \it{data layer} \\
    \hline
  \end{tabular}
  %
  }
  %
\end{center}
  %
\end{example}


\begin{flushleft}
  %% \scalebox{1}{\ldots\ is \emph{productive} and specifies
  %%              the \emph{ternary Thue--Morse stream}:}\\[1.5ex]
  %% \hspace*{\fill}
  \scalebox{1}{
  $
  \strcf{Q}
  \infred
  \strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{
  \strcns{\datf{a}}{\strcns{\datf{c}}{\strcns{\datf{b}}{
  \strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{
  \strcns{\datf{b}}{\strcns{\datf{a}}{\strcns{\datf{c}}{
  \ldots}}}}}}}}}}}}
  $%
                  }
  \hspace*{\fill}\mbox{}
  %
\end{flushleft}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{comment}

\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification (flat, non-pure)}

\begin{example}[Pascal's triangle stream]
  %
  \vspace*{0.5ex}
  %
\begin{center}
\scalebox{1}{ 
  \renewcommand{\arraystretch}{1.3}
  \begin{tabular}{r@{\hspace{0ex}}r@{\extracolsep{.5ex}}c@{\extracolsep{.5ex}}lr}
    \hline
    \multicolumn{4}{c}{
    $\strcf{P} \red \strcns{\numzer}{\strcns{\numsuc{\numzer}}{\funap{\strff{g}}{\strcf{P}}}}$} 
    \\
    &$\funap{\strff{g}}{\strcns{\numsuc{x}}{\strcns{y}{\astr}}}$ 
    &$\red$& $\strcns{\numadd{\numsuc{x}}{y}}{\funap{\strff{g}}{\strcns{y}{\astr}}}$%  & \text{\textit{stream layer}}
    & {\it stream layer} \\
    &$\funap{\strff{g}}{\strcns{\numzer}{\astr}}$ 
    &$\red$& $\strcns{\numzer}{\strcns{\numsuc{\numzer}}{\funap{\strff{g}}{\astr}}}$
    \\
    \hline
    &$\numadd{x}{\numsuc{y}}$ 
    &$\red$& $\numsuc{\numadd{x}{y}}$ 
    & \multirow{2}{*}{\text{\textit{data layer}}}
    \\[-0.5ex]
    &$\numadd{x}{\numzer}$ 
    &$\red$& $x$
    \\
    \hline
  \end{tabular}
}
\end{center}
  %
  \mbox{}\\[-0.5ex]
  %
\end{example}
 

\begin{flushleft}
  %% \scalebox{1}{is a \emph{productive} stream definition
  %%              of the \emph{Pascal's triangle}:}\\[1.5ex]
  %% \hspace*{\fill}
  \scalebox{1}{
  $
  \strcf{P} \infred \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{0}}\strcns{\datf{1}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{1}}\strcns{\datf{2}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{1}}\strcns{\datf{3}}{
                 \strcns{\datf{3}}{\strcns{\datf{1}}{\strcns{\datf{0}}{
                   \ldots}}}}}}}}}}}}
  $
                  }\hspace*{\fill}
\end{flushleft}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification (pure)}

\begin{example}[Thue--Morse stream]
  %
  \vspace*{0.5ex}
  %
\begin{center}
\scalebox{1}{ 
\renewcommand{\arraystretch}{1.3}
\begin{tabular}{r@{\hspace*{1.5ex}}cr}
  \hline
  &
  $\morse \red 
   \strcns{\datf{0}}{\strcns{\datf{1}}{\strfff{f}{\strtl{\morse}}}}$ 
  \\[-0.0ex]
  &
  $\strfff{f}{\strcns{\datf{0}}{\astr}} 
     \red
   \strcns{\datf{0}}{\strcns{\datf{1}}{\strfff{f}{\astr}}}
  $  
  & {\it stream layer}
  \\[-0.0ex]
  &
  $\strfff{f}{\strcns{\datf{1}}{\astr}} 
     \red
   \strcns{\datf{1}}{\strcns{\datf{0}}{\strfff{f}{\astr}}}
  $
  \\[-0.0ex]
  &
  $\strtl{\strcns{x}{\astr}} \red \astr$
  \\[-0.0ex]
  \hline
  & & {\it data layer}
  \\
  \hline
\end{tabular}
               }
\end{center}
  %
  \mbox{}\\[-0.5ex]
  %
\end{example}
 

\begin{flushleft}
  \scalebox{1}{
  $
  \morse \infred \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{1}}\strcns{\datf{0}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{0}}\strcns{\datf{1}}{
                 \strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{0}}\strcns{\datf{1}}{
                 \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{1}}\strcns{\datf{0}}{
                   \ldots}}}}}}}}}}}}
  $
                  }\hspace*{\fill}
\end{flushleft}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification (pure)}

\begin{example}[Thue--Morse stream]
  %
  \vspace*{2.5ex}
  %
\begin{center}
\scalebox{1}{
\renewcommand{\arraystretch}{1}
\begin{tabular}{cr}
  \hline
  \rule{0pt}{2ex}
  $\morse \red \strcns{\datsymb{0}}{\strzip{\strinv{\morse}}{\strtl{\morse}}}$
  & 
  \multirow{4}{*}{{\it stream layer}}
  \\
  $\strtl{\strcns{x}{\astr}} \red \astr$ & \\[-0.0ex]
  $\strzip{\strcns{x}{\astr}}{\bstr} \red \strcns{x}{\strzip{\bstr}{\astr}}$ 
  \\[-0.0ex]
  $\strinv{\strcns{x}{\astr}} \red \strcns{\funap{\datsymb{i}}{x}}{\strinv{\astr}}$ & \\
  \hline
  \rule{0pt}{2ex}
  $\funap{\datsymb{i}}{\datsymb{0}} \red \datsymb{1} \quad\quad \funap{\datsymb{i}}{\datsymb{1}} \red \datsymb{0}$
  & {\it data layer} \\
  \hline
\end{tabular}
               }
\end{center}
  %
  \mbox{}\\[0.5ex]
  %
\end{example}
 
\begin{flushleft}
  %% \scalebox{1}{This is a \emph{productive} stream spec
  %%              for the \emph{Thue--Morse stream}:}\\[1.5ex]
  %% \hspace*{\fill}
  \scalebox{1}{
  $
  \morse \infred \strcns{0}{\strcns{1}{\strcns{1}\strcns{0}{
                 \strcns{1}{\strcns{0}{\strcns{0}\strcns{1}{
                 \strcns{1}{\strcns{0}{\strcns{0}\strcns{1}{
                 \strcns{0}{\strcns{1}{\strcns{1}\strcns{0}{
                   \ldots}}}}}}}}}}}}
  $
                  }
\end{flushleft}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification (pure)}  

\begin{example}[ternary Thue--Morse stream]
%
%\vspace*{1.5ex}
%
\begin{center}
  %
\scalebox{1}{
  %
  \begin{tabular}{r@{\hspace{1.5ex}}r@{\extracolsep{1ex}}c@{\extracolsep{1ex}}lr}
    %
    \hline
    \multicolumn{4}{c}{\rule{0pt}{2ex}
    $\strcf{Q} \red \funap{\strff{diff}}{\strcf{M}}$}
    &\qquad\multirow{6}{*}{\it{stream layer} }
    \\[0ex]
    \multicolumn{4}{c}{
    $\strcf{M} \red \strcns{\datf{0}}{\strzip{\strinv{\strcf{M}}}{\strtl{\strcf{M}}}}$
    }
    \\
    & \rule{0pt}{2ex} $\strzip{\strcns{x}{\astr}}{\bstr}$ 
    &$\red$& $\strcns{x}{\strzip{\bstr}{\astr}}$ \\[-0ex]
    & $\strinv{\strcns{x}{\astr}}$ 
    &$\red$& $\strcns{\inv{x}}{\strinv{\astr}}$
    &
    \\[0ex]
    & $\strtl{\strcns{x}{\astr}}$ &$\red$& $\astr$ 
    \\[0ex]
    % 00 -> a , 01 -> b , 10 -> c, 11 -> a
    &$\strdiff{\strcns{x}{\strcns{y}{\astr}}}$ 
    &$\red$& $\strcns{\abc{x}{y}}{\strdiff{\strcns{y}{\astr}}}$
    \\[0ex]
    \hline
    & \rule{0pt}{2ex}
      $\inv{\datf{0}} \red \datf{1}$ & &$\inv{\datf{1}} \red \datf{0}$ \\[0ex]
    & $\abc{\datf{0}}{\datf{0}} \red \datf{b}$ & &$\abc{\datf{0}}{\datf{1}} \red \datf{a}$ 
    & \it{data layer}
    \\[0ex]
    & $\abc{\datf{1}}{\datf{0}} \red \datf{c}$ & &$\abc{\datf{1}}{\datf{1}} \red \datf{b}$ \\
    \hline
  \end{tabular}
  %
  }
  %
\end{center}
  %
  %\vspace*{0.75ex}
  %
\end{example}

\begin{flushleft}
  %% \scalebox{1}{\ldots\ is \emph{productive} and specifies
  %%              the \emph{ternary Thue--Morse stream}:}\\[1.5ex]
  %% \hspace*{\fill}
  \scalebox{1}{
  $
  \strcf{Q}
  \infred
  \strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{
  \strcns{\datf{a}}{\strcns{\datf{c}}{\strcns{\datf{b}}{
  \strcns{\datf{a}}{\strcns{\datf{b}}{\strcns{\datf{c}}{
  \strcns{\datf{b}}{\strcns{\datf{a}}{\strcns{\datf{c}}{
  \ldots}}}}}}}}}}}}
  $%
                  }
  \hspace*{\fill}\mbox{}
  %
\end{flushleft}


\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification (friendly-nesting)}
  
\newcommand{\myvspace}{\rule{0pt}{2.2ex}}  
\renewcommand{\arraystretch}{1.25}
  %  
  
\begin{example}[convolution product $\boldsymbol{\times}$]
  %
  \vspace*{-0.5ex}
  %
\begin{center}  
  %
\scalebox{.93}{$  
  %
  \begin{array}{cr} 
    %
    \hline
    %
    \nats \red \strcns{\datf{0}}{\convprod{\ones}{\ones}}
    & \quad
    \multirow{5}{*}{{\it stream layer}}
    \\
    \ones \red \strcns{\numsuc{\datf{0}}}{\ones}
    \\
    \bfunap{\strff{\boldsymbol{\times}}}%
     {\strcns{x}{\astr}}{\strcns{y}{\bstr}}
    \red   \strcns{\nummult{x}{y}}%
                    {\stradd{ \strtimes{\bstr}{x} }%
                            { \bfunap{\strff{\boldsymbol{\times}}}%
                                     {\astr}{\strcns{y}{\bstr}} } }
    \\
    \strtimes{\strcns{x}{\astr}}{y}%
        \red  \strcns{\nummult{x}{y}}{\strtimes{\astr}{y}}                                                               
    \\
    \stradd{\strcns{x}{\astr}}{\strcns{y}{\bstr}}%
        \red   \strcns{\numadd{x}{y}}%
                        {\stradd{\astr}{\bstr}}
    %
    \\%[3.5ex]
    %
    \hline%
    %
    \begin{array}{cc}
      %
      \numadd{x}{\datf{0}} \red   x    
      & 
      \numadd{x}{\numsuc{y}}   \red   \numsuc{\numadd{x}{y}} 
      \\
      \nummult{x}{\datf{0}} \red   \datf{0}  
      & 
      \nummult{x}{\numsuc{y}}   \red   
          \numadd{ \nummult{x}{y} }{x}
      %
    \end{array}
    %
    & \text{{\it data layer}} 
    \\
    \hline
    %
  \end{array}
  %
  $}
  %
  \vspace*{-1.5ex}
  %
\end{center}
  %
\end{example}

$\sconvprod$ defines % the \emph{convolution product}
the stream operation
$ \pair{\astr}{\bstr} \mapsto \astr\times\bstr $:
%
\begin{align*}
  %
  \strnth{({\astr}\times{\bstr})}{i} 
    & = \sum_{j=0}^i \strnth{\astr}{j}\cdot\strnth{\bstr}{i-j} 
  & & \text{(for all $i\in\nat$)}
  %
\end{align*}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%------------------------------------------------------------------------
%------------------------------------------------------------------------
\section{Map}
%------------------------------------------------------------------------
%------------------------------------------------------------------------


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Map of Stream Specifications}  
    
\begin{center}
  %
  \scalebox{1.15}{ 
    \includegraphics{figs/pstricks/pnp}
              }
  %
\end{center}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%------------------------------------------------------------------------
%------------------------------------------------------------------------
\section{Results}
%------------------------------------------------------------------------
%------------------------------------------------------------------------


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Results, Put into Perspective}

\vspace*{-0.5ex}
%
\begin{itemize}%[<+->]
    %
  \item
  \chocolate{Previous Approaches}
  (\forestgreen{Wadge}, \forestgreen{Sijtsma}, \forestgreen{Coquand},
   \forestgreen{Telford/Turner},  
   \forestgreen{Gimenez}, \forestgreen{Hughes/Pareto/Sabry},
   \forestgreen{Buchholz}):
  \emph{sufficient conditions} for productivity,
  not automatable or only for a limited subclass
    %
    \vspace*{0.5ex}
    %
  \item
  \chocolate{FCT'07} (\forestgreen{E/G/H/Isihara/Klop}):
  \emph{decision algorithm} for productivity of \darkmagenta{pure SCS{s}} 
     %
    \vspace*{0.5ex}
    %
  \item
  \chocolate{New Results}:
    %
    \begin{enumerate}
      %
      \vspace*{0.75ex}
        %
      \item\label{item:summary:flat}
        a \emph{computable, d-o optimal,
        sufficient condition} for productivity\\
        of \darkmagenta{flat} stream spec's;
        %
        \vspace*{0.5ex}
        %
      \item\label{item:summary:pure}
        a \emph{decision method} for productivity on 
        \darkmagenta{pure} stream spec's\\
        % with \darkmagenta{duplication/additional supply}
        % in stream arg's 
        (significant extension of FCT);
        %
        \vspace*{0.5ex}
        %
      \item\label{item:summary:friendly} 
        an extension of~\ref{item:summary:flat}
        to \darkmagenta{friendly nesting} stream spec's,
        disregarding d-o optimality;
        %
        \vspace*{0.5ex}
        %
      \item a tool automating~\ref{item:summary:flat}, \ref{item:summary:pure} 
        and~\ref{item:summary:friendly} available at:
        \href{http://localhost/productivity/}%
         {\emph{\tt http://infinity.few.vu.nl/productivity}}.
         %
   \end{enumerate}
   %
\end{itemize}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%------------------------------------------------------------------------
%------------------------------------------------------------------------
\section{Decision Algorithm}
%------------------------------------------------------------------------
%------------------------------------------------------------------------


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Deciding D-O Productivity}


  \begin{enumerate}
      %
      \vspace*{1.65ex}
      %
    \item  \chocolate{Input}: a \emph{flat} stream specification $\atrs$.
      %
      \vspace*{1.65ex}
      %
    \item  \chocolate{Stream function translation}:
      for the stream functions $\strff{f}$ in $\atrs$,
      compute their d-o lower bounds
      $\trnsl{\strff{f}} \funin \conat \to \conat$
      \\ \hspace*{\fill}
      (\emph{periodically increasing functions}).
      %
      \vspace*{1.65ex}
      %
    \item  \chocolate{Stream constant translation}: using (2),
      translate the root $\rootsc$ of $\atrs$\\
      into a \emph{production term} $\trnsl{\rootsc}$.
      %
      \vspace*{1.65ex}
      %
    \item  \chocolate{Production calculation}:
      compute the production $\netprd{\trnsl{\rootsc}}$ of $\trnsl{\rootsc}$\\
      in a \emph{production calculus} (by a {confluent, terminating TRS}).
      %
      \vspace*{1.65ex}
      %
    \item \chocolate{Decision taking}:
      \parbox[t]{200pt}{%
           if $\netprd{\trnsl{\rootsc}}=\infty$
             then $\atrs$ is \magenta{d-o productive},\\
             else $\atrs$ is \magenta{not d-o productive}.%
                        }
      %
  \end{enumerate}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  


%------------------------------------------------------------------------
%------------------------------------------------------------------------
\section{Productivity Tool}
%------------------------------------------------------------------------
%------------------------------------------------------------------------


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Productivity Tool}

  \vspace*{0.5ex}
  %
  \begin{itemize}
    %
    \item  \emph{Translation and reduction tool} (Haskell-based).\\[0.5ex]
      %
      Use it at:
      \href{http://localhost/productivity}
           {\emph{\tt http://infinity.few.vu.nl/productivity}} 
      %
  \end{itemize}

    
  %\vspace*{-0.5ex}
  %
  \begin{align*}
    %
    \href{http://localhost/productivity/\#thuemorse_alternative}{\morse} 
      &= \strcns{\datsymb{0}}{\strzip{\strinv{\morse}}{\strtl{\morse}}}
    \\
    \href{http://localhost/productivity/\#thuemorse_alternative}{\terprd{\atrs}{\morse}}
      &= \netprd{\trnsl{\morse}} 
       = \boldsymbol{\conattop}
    \\[2.5ex]
    %
    \href{http://localhost/productivity/\#J}{\joerg} 
      &= \strcns{\datsymb{0}}{\strcns{\datsymb{1}}{\strev{\joerg}}}
    \\
    \href{http://localhost/productivity/\#J}{\terprd{\atrs}{\joerg}}
      & = \netprd{\trnsl{\joerg}}
        = 4
    \\[2.5ex]
    %
    \href{http://localhost/productivity/\#D}{\dimitri} 
      &= \strcns{\datsymb{0}}{\strcns{\datsymb{1}}{\strcns{\datsymb{0}}{
                    \strzip{\stradd{\strtl{\dimitri}}{\strtl{\strtl{\dimitri}}}}
                           {\strev{\strtl{\dimitri}}} }}}
    \\
    \href{http://localhost/productivity/\#D}{\terprd{\atrs}{\dimitri}}
      &= \netprd{\trnsl{\dimitri}}
       = \boldsymbol{\conattop}
      %
  \end{align*}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




%------------------------------------------------------------------------
%------------------------------------------------------------------------
%\section[Production Calculus]{The Production Calculus}
%------------------------------------------------------------------------
%------------------------------------------------------------------------


%------------------------------------------------------------------------
%------------------------------------------------------------------------
%\section[Translation]{Translation into Production Terms}
%------------------------------------------------------------------------
%------------------------------------------------------------------------


%------------------------------------------------------------------------
%------------------------------------------------------------------------
%\section[Deciding D-O Productivity]{Deciding Data-Oblivious Productivity}
%------------------------------------------------------------------------
%------------------------------------------------------------------------


%------------------------------------------------------------------------
%------------------------------------------------------------------------
%\section[Conclusion]{Conclusion}
%------------------------------------------------------------------------
%------------------------------------------------------------------------



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{}

   \vspace*{\fill}
   %
   \hspace{\fill}%
   \scalebox{1.6}{\forestgreen{\bf Thanks for your attention!}}%
   \hspace*{\fill}\mbox{}
   %
   \label{lastslide}
   %
   \vspace*{\fill}

 %% \only<7>{
 %% \begin{center}
 %% \large{Thank you!}
 %% \end{center}
 %% }

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Our Papers and Tools.}

  \vspace*{0.5ex}
  %
  Please visit \href{http://localhost/productivity/}%
         {\emph{\tt http://infinity.few.vu.nl/productivity}}\\
  to find: 
  %
  \vspace*{1.5ex}
  %
  \begin{itemize}
    %
    \item 
      Endrullis, Grabmayer, Hendriks, Isihara, Klop:\\
      \emph{Productivity of Stream Definitions},
      Proceedings of FCT~2007, LNCS~4637, pages~274--287, 2007.
      %
      \vspace*{0.75ex}
      %
    \item  
      Endrullis, Grabmayer, Hendriks, Isihara, Klop:\\
      \emph{Productivity of Stream Definitions},
      Logic Group Preprint 268,\\
      Universiteit Utrecht, November 2008.
      %
      \vspace*{0.75ex}
      %
    \item Endrullis, Grabmayer, Hendriks:\\
      \emph{Data-Oblivious Stream Productivity},
      LPAR~2008.
      %
      \vspace*{0.75ex}
      %
    \item access to our tools:
      %
      \begin{itemize}
        %
        \item Endrullis: tool implementing the\\ 
          \hspace*{3ex}  
          \chocolate{decision algorithm
                     for data-oblivious productivity};
          %
        \item Isihara: \chocolate{pebbleflow visualization} tool.

        %
      \end{itemize} 
      %
  \end{itemize}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\end{document}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%





\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Productivity Decision}

\emph{Productivity of Stream Definitions}
(E, G, H, Isihara, Klop), FCT'07:

\vspace*{0.5ex}
%
\begin{itemize}
  %
  \item a \chocolate{decision algorithm for productivity}
    on the class of 
    \emph{stream constant specifications (SCS{s}}.
    %
    \vspace*{0.85ex}
    %
  \item large and natural class: stream functions used 
    in pure stream spec's contain all \emph{automatic sequences}
    (Allouche, Shallit). 
    %
    \vspace*{0.85ex}
    %
  \item Idea behind the decision algorithm:
    %
    \begin{itemize}
        %
        \vspace*{0.25ex}
        %
      \item The process of evaluation of a pure stream spec can
        be modelled by dataflow of \emph{pebbles} in a finite
        \emph{pebbleflow net}.
        %
        \vspace*{0.25ex}
        %
      \item The production of a pebbleflow net associated with
        a pure stream spec (amount of pebbles the net can produce
        at its output port) can be calculated by reducing nets
        to trivial nets.
        %
    \end{itemize}
    %
\end{itemize}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%





\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Map of Stream Specifications}  

    
\begin{center}
  %
  \scalebox{1.15}{ 
    \includegraphics{figs/pstricks/pnp}
              }
  %
\end{center}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Production Terms}

\vspace*{-0.45ex}
%
\begin{definition}
  %
  For $\nam$ a set of recursion variables,
  the set $\net$ of \emph{production terms} is generated by:
  \[
    \anet
    \BNFis
    \netsrc{k}
    \BNFor
    \netvar{\avar}
    \BNFor
    \netbox{\aiosq}{\anet}
    \BNFor
    \netrec{\anam}{\anet}
    \BNFor
    \netmeet{\anet}{\anet}
  \]
  where $\anam\in\nam$, $\aiosq\in\sqpair$,
  and $\netsrc{k}$ is a \emph{numeral} for $k\in\conat$.
  %
  %% For $\anet_1,\ldots,\anet_n\in\net$ and $n\in\nat$, 
  %% we use $\netmeetn{n}{\anet_1,\ldots,\anet_n}$
  %% as shorthand for the production term
  %% $\netmeet{\anet_1}{\netmeet{\anet_2}{\ldots,\netmeet{\anet_{n-1}}{\anet_n}}}$.

  \vspace*{0.5ex}
  %
  The \emph{production} $\chocolate{\netbhv{\black{\anet}}} \in \conat$
  of a closed production term $\anet \in \net$ is defined by 
  induction on the term structure,
  interpreting:
  \begin{itemize}
    %
    \item $\snetrec$ as the least fixed point operator,
    \item $\aiosq$ as $\siosqprd{\aiosq}$, 
    \item $\netsrc{k}$ as $k$, and 
    \item $\snetmeet$ as $\min$.
    %
  \end{itemize}
  %
  \emph{$r$-ary Gates}:  production term contexts 
    $\netmeetn{r}{\netbox{\iaiosq{1}}{\porti{1}},\ldots,\netbox{\iaiosq{r}}{\porti{r}}}$.
  %
\end{definition}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Reduction $\scolred$}

\begin{definition}
  The \emph{reduction relation 
  $\scolred$ on production terms}
  is defined as the compatible closure of: 
  %
  \begin{align*}
    %
    \netbox{\iaiosq{1}}{\netbox{\iaiosq{2}}{\anet}}
    & \red \netbox{\iosqcmp{\iaiosq{1}}{\iaiosq{2}}}{\anet}
    \pagebreak[0]\\
    \netbox{\aiosq}{\netmeet{\ianet{1}}{\ianet{2}}}
    & \red \netmeet{\netbox{\aiosq}{\ianet{1}}}{\netbox{\aiosq}{\ianet{2}}}
    \pagebreak[0]\\
    \netrec{\anam}{\netmeet{\ianet{1}}{\ianet{2}}}
    & \red \netmeet{\netrec{\anam}{\ianet{1}}}{\netrec{\anam}{\ianet{2}}}
    \pagebreak[0]\\
    \netrec{\anam}{\anet}
    & \red \anet
    \qquad \text{if $\anam\not\in\netfv{\anet}$}
    \pagebreak[0]\\
    \netrec{\anam}{\netbox{\aiosq}{\anam}}
    & \red \netsrc{\iosqfix{\aiosq}}
    \pagebreak[0]\\
    \netrec{\anam}{\netvar{\anam}}
    & \red \netsrc{0}
    \pagebreak[0]\\
    \netbox{\aiosq}{\netsrc{k}}
    &\red
    \netsrc{\iosqprd{\aiosq}{k}}
    \pagebreak[0]\\
    \netmeet{\netsrc{k_1}}{\netsrc{k_2}}
    & \red \netsrc{\comin{k_1,k_2}}  
    %
  \end{align*}
  %
\end{definition}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Reduction $\scolred$}

Properties of $\scolred$:
%
\begin{itemize}
  %
  \item production preserving;
    %
  \item confluent and terminating;
    %
  \item normal forms are numerals.
  %
\end{itemize}

\vspace*{2ex}
%
\begin{theorem}
  %
  For all $\anet\in\net$:
  \[ \netprd{\anet}=k \; ,\]
  where $\netsrc{k}$ is the uniquely determined
  $\scolred$-normal form of $\anet$.
  %
\end{theorem}


\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Translation into Production Terms}


%\begin{itemize}
  %
  %\item
    We use a translation 
    that maps every \forestgreen{flat} stream spec $\atrs$
    with root $\rootsc$ to a \emph{production term} $\trnsl{\rootsc}$
    such that
    %
    \begin{equation*}
      %
      \doLow{\atrs}{\rootsc} = \netbhv{\trnsl{\rootsc}} \; .
      %
    \end{equation*}
    %
%\end{itemize}


\begin{itemize}
  %
  \item \emph{function layer translation}:
    Obtain a family $\{\trnsl{\astrfun} \}_{\astrfun\in\Ssf}$
    of gates such that, for every $\strff{f}\in\Ssf$, the gate $\fgate$
    represents the data-oblivious lower bound of $\strff{f}$ in $\atrs$.

    \vspace*{0.5ex}
    %
    (Involves solving an originally infinite `\ioterm\ specification'.)
    %
    % (Involves solving, for each argument place in $\strff{f}$
    %  an originally infinite `\ioterm\ specification' which
    %  specifies the data-oblivious lower bound in that argument place.)
    %
    \vspace*{1ex}
    %
  \item \emph{stream layer translation}:
    Using the family $\strff{f}\in\Ssf$ of gates, obtain 
    a production term $\trnslF{\rootsc}{\afam}$ such that
    $ \netbhv{\trnslF{\rootsc}{\afam}} = \doLow{\atrs}{\rootsc} $. 

    \vspace*{0.5ex}
    %
    (Involves expanding the stream layer rules step by step and
     a finite loop-checking procedure.)
    %
\end{itemize}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specifications (Properties II)}

A stream spec $\atrs$ is called
%
\begin{itemize}
  %
  \item \magenta{friendly-nesting}:
    all rules in the function layer $\Rsf$ are \emph{flat},
    or contained in a subset $\tilde{R}\subset\Rsf$ of 
    \emph{friendly-nesting} rules:\\
    every $\rho\in\tilde{R}$
    %
    \begin{itemize}
      %
      \item consumes in each stream argument at most one element,
      \item produces at least one, and
      \item all defining rules of stream functions occurring on the
        right-hand side of $\rho$ are again in $\tilde{R}$.
        %
    \end{itemize}
    %
\end{itemize}



%
\begin{example}
%
\begin{center}
  $
  \bfunap{\strff{f}}{\strcns{x}{\astr}}{\bstr}
     \red 
      \strcns{x}{\strcns{x}{\funap{\strff{g}}{\bfunap{\strff{f}}{\astr}{\strcns{x}{\bstr}}}}}
  $
  \\[0.5ex]
  $
  \funap{\strff{g}}{\strcns{x}{\astr}}
     \red
      \strcns{x}{\funap{\strff{g}}{\strcns{x}{\bfunap{\strff{f}}{\astr}{\astr}}}}
  $
\end{center}
%
\end{example}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Stream Specification (flat, non-pure)}
  
\newcommand{\myvspace}{\rule{0pt}{2.2ex}}  
  %  
\begin{example}[Hamming numbers]
  %  
\begin{center}  
  %
\scalebox{0.8}{$ 
  \renewcommand{\arraystretch}{1.25} 
  %
\begin{array}{cr}
  \hline
    \myvspace%
     \strcf{H} 
    \to 
    \strcns{\trmrep{\datf{1}}}{
      \strmerge{
        \strtimes{\strcf{H}}{\trmrep{\datf{2}}}}{
        \strmerge{
          \strtimes{\strcf{H}}{\trmrep{\datf{3}}}}{
          \strtimes{\strcf{H}}{\trmrep{\datf{5}}}
        }
      }
    }
  \\
  %
  \begin{array}{rcl}
  \myvspace%  
  \strtimes{\strcns{x}{\astr}}{y} &\to& \strcns{\nummult{x}{y}}{\strtimes{\astr}{y}}
  \\
  \strmerge{\strcns{x}{\astr}}{\strcns{y}{\bstr}} &\to& \aux{\astr}{\bstr}{x}{y}{\compare{x}{y}}
  \\
  \aux{\astr}{\bstr}{x}{y}{\ltsymb} &\to& \strcns{x}{\strmerge{\astr}{\strcns{y}{\bstr}}}
  \\
  \aux{\astr}{\bstr}{x}{y}{\eqsymb} &\to& \strcns{x}{\strmerge{\astr}{\bstr}}
  \\
  \aux{\astr}{\bstr}{x}{y}{\gtsymb} &\to& \strcns{y}{\strmerge{\strcns{x}{\astr}}{\bstr}}
  \end{array}
  &
  \hspace{-2.5ex}
  \raisebox{1ex}{\text{{\it stream layer}}}
  \\[6ex]
  \hline%
  %
  \begin{array}{rclcrcl}
  \myvspace%  
  \compare{\numzer}{\numzer} &\to& \eqsymb
  &\hspace{1em}&
  \numadd{\numzer}{y} &\to& y
  \\
  \compare{\numzer}{\numsuc{y}} &\to& \ltsymb
  &&
  \numadd{\numsuc{x}}{y} &\to& \numsuc{\numadd{x}{y}}
  \\
  \compare{\numsuc{x}}{\numzer} &\to& \gtsymb
  &&
  \nummult{\numzer}{y} &\to& \numzer
  \\
  \compare{\numsuc{x}}{\numsuc{y}} &\to& \compare{x}{y}
  &&
  \nummult{\numsuc{x}}{y} &\to& \numadd{y}{\nummult{x}{y}}
  \\
  \end{array}
  & 
  \hspace{-2.5ex}
  \text{{\it data layer}}
  \\[5ex]
  \hline%
\end{array}
  $
  }
  %
\end{center} 
  %
\end{example} 

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Data-Oblivious Analysis}

\begin{center}
  %
\scalebox{1}{
\renewcommand{\arraystretch}{1.25}
\begin{tabular}{r@{\hspace{1.5ex}}cr}
  \hline
  &
  $\strcf{T} \red \funap{\strff{f}}{\strcns{\datf{0}}{\strcns{\datf{1}}{\strcf{T}}}}$
  & \multirow{3}{*}{\it stream layer}
  \\
  $(\rho_{\astrfunsub\datf{0}}):$\hspace*{2ex}
  &
  $\strfunap{f}{ \strcns{\datf{0}}{\strcns{x}{\astr}} } 
   \red \strcns{\datf{0}}{\strcns{\datf{1}}{\strfunap{f}{\astr}}}$
  \\
  $(\rho_{\astrfunsub\datf{1}}):$\hspace*{2ex} 
  &
  $\strfunap{f}{\strcns{\datf{1}}{\strcns{x}{\astr}}} 
   \red \strcns{x}{\strfunap{f}{\astr}}$
  &
  \\
  \hline
  & & {\it data layer}\\
  \hline
\end{tabular}
  %
  }
  %
\end{center}


This specification is \emph{productive}:
%
\begin{equation*}
  %
  \strcf{T} 
    \mred \strcns{\datf{0}}{\strcns{\datf{1}}{\funap{\strff{f}}{\strcf{T}}}}
    \mred \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{1}}{\funap{\strff{f}}{\funap{\strff{f}}{\strcf{T}}}}}}}
    \mred \ldots 
    \infred \strcns{\datf{0}}{\strcns{\datf{1}}{\strcns{\datf{0}}{\strcns{\datf{1}}{\ldots}}}} \; ,
    %
\end{equation*}
%
but, disregarding the identity of data, the rewrite sequence:
%
\begin{equation*}
  %
  \strcf{T}
    \red \funap{\strff{f}}{\strcns{\trspeb}{\strcns{\trspeb}{\strcf{T}}}}
    \red^{\rho_{\astrfunsub\datf{1}}}
    \strcns{\trspeb}{\funap{\strff{f}}{\strcf{T}}}
    \mred 
    \ldots
    \infred \strcns{\trspeb}{\funap{\strff{f}}{\strcns{\trspeb}{\funap{\strff{f}}{\strcns{\trspeb}{\funap{\strff{f}}{\ldots}}}}}} \; .
    %
\end{equation*}
%
is possible.
Hence the specification is 
\alert{not data-obliviously productive}.

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \frametitle{Data-Oblivious Rewriting}

A \emph{two-player game}:
%
\begin{itemize}
  %
  \item \emph{rewrite player} $\mathcal{R}$ 
    can perform usual term rewriting steps
    %
  \item \emph{data-exchange player} $\sdg$ can exchange 
        data elements arbitrarily
        %
\end{itemize}

\begin{example}
    %% [%
    %% $\strcf{T} \red \funap{\strff{f}}{\strcns{\datf{0}}{\strcns{\datf{1}}{\strcf{T}}}}, \;
    %% \strfunap{f}{ \strcns{\datf{0}}{\strcns{x}{\astr}} } \red \strcns{\datf{0}}{\strcns{\datf{1}}{\strfunap{f}{\astr}}}, \;
    %% \strfunap{f}{\strcns{\datf{1}}{\strcns{x}{\astr}}} \red \strcns{x}{\strfunap{f}{\astr}}
    %% $]
  %
  \begin{center}
    %
    $\strcf{T} \red \funap{\strff{f}}{\strcns{\datf{0}}{\strcns{\datf{1}}{\strcf{T}}}},\quad
    \strfunap{f}{ \strcns{\datf{0}}{\strcns{x}{\astr}} } \red \strcns{\datf{0}}{\strcns{\datf{1}}{\strfunap{f}{\astr}}},\quad
    \strfunap{f}{\strcns{\datf{1}}{\strcns{x}{\astr}}} \red \strcns{x}{\strfunap{f}{\astr}}
    $ 
  \end{center}
  %
  Data-oblivious rewriting of $\strcf{T}$,
  a \emph{$\sdg$-game for $\mathcal{R}$}:
  %
  \vspace{-1ex}
  \begin{center}
    %
    \scalebox{1}{\includegraphics{figs/pstricks/doexample}}
    %
  \end{center}
  %
  \vspace{-1ex}
  %
\end{example}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{definition}
  %
  The \emph{data-oblivious lower bound} on the production of a term $s$ is:
  %in a stream spec $\atrs$:
  \begin{equation*}
    %
    \doLow{\atrs}{\astrtrm} \;\defdby\;
      \inf\Bigl\{ \funap{\text{max-stream-prefix-in}}{\Gamma} \;\Big|\;
              \parbox[c]{115pt}{%
                \hspace*{\fill}$\Gamma$ a \emph{fair} $\sdg$-game on $\atrs$,
                  \hspace*{\fill}\mbox{}\\
                $\sdg$ data-exchange strategy%
                                }
      \Bigr\}
    %
  \end{equation*}
  %
  A stream spec~$\atrs$ is \emph{data-obliviously productive} if $\doLow{\atrs}{\rootsc} = \infty$.
\end{definition}

\begin{proposition}[Data-oblivious productivity implies productivity]
  \begin{equation*}
    %
    \doLow{\atrs}{s} \le \terprd{\atrs}{s} \; .
    %
  \end{equation*}
  %
  %That is, data-oblivious productivity implies productivity.
\end{proposition}

\begin{example}[%
  $
  %\atrs = \bigl\{
      \strcf{T} \red \funap{\strff{f}}{\strcns{\datf{0}}{\strcns{\datf{1}}{\strcf{T}}}}, \;
      \strfunap{f}{ \strcns{\datf{0}}{\strcns{x}{\astr}} } \red \strcns{\datf{0}}{\strcns{\datf{1}}{\strfunap{f}{\astr}}}, \;
      \strfunap{f}{\strcns{\datf{1}}{\strcns{x}{\astr}}} \red \strcns{x}{\strfunap{f}{\astr}}
  %          \bigr\}
  $]
  %
  For this stream specification $\atrs$ we find:
  $\doLow{\atrs}{\strcf{T}} = 1$.\\
  Hence $\atrs$ is \alert{not data-obliviously productive}.
  %
\end{example}

\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
